Skip to content

Fix declaration order and enum mangling issues#681

Open
tahina-pro wants to merge 7 commits intoFStarLang:masterfrom
tahina-pro:_taramana_decl_order
Open

Fix declaration order and enum mangling issues#681
tahina-pro wants to merge 7 commits intoFStarLang:masterfrom
tahina-pro:_taramana_decl_order

Conversation

@tahina-pro
Copy link
Member

@tahina-pro tahina-pro commented Feb 18, 2026

This PR fixes C and Rust extraction issues that have been hitting EverParse since moving ahead of Karamel's "last known good" commit for EverParse, fb36fec, and which #679 has not entirely fixed.

Changes introduced by this PR, including unit test cases, have been entirely AI-generated by GitHub Copilot CLI using Claude Opus 4.6 (apart from a few purely cosmetic changes of mine.) Commit descriptions contain more details about the issues, their fixes and the corresponding unit test cases.

Full EverParse CI works with 660f525 : https://github.com/tahina-pro/quackyducky/actions/runs/22151241820

tahina-pro and others added 7 commits February 18, 2026 04:52
…order

The hoist pass in Simplify.ml builds a field_types table from DType
declarations, then uses it when processing DFunction bodies. When
monomorphization emits types after the functions that reference them,
Hashtbl.find crashes with Not_found.

Use Hashtbl.find_opt with a safe default (false = not an array type)
instead. This is correct because the lookup only determines whether a
struct field is an array type for hoisting purposes.

Co-authored-by: Copilot <[email protected]>
The changes in FStarLang#676 (commit c1e092f) introduced three problems for
non-polymorphic types:

1. The fast-path in visit_node skipped non-polymorphic types that hadn't
   been seen yet, deferring them to their source position. This broke
   DFS dependency ordering: types could appear after the types that use
   them by value.

2. The 'if args <> [] || cgs <> []' guards prevented visit_node from
   recording non-polymorphic types, forcing them to be emitted at their
   source position via visit_decl instead of in DFS order.

3. The visit_decl handler for non-polymorphic DTypes used Gray/Black
   state management and appended the visited declaration, instead of
   delegating to visit_node for proper DFS ordering.

4. Type arguments were visited with the caller's under_ref flag, which
   could trigger full processing of types that are actually used behind
   pointers inside the parameterized type (e.g., slice<T> stores T*).

Fix: restore the old DFS-based ordering by (1) only fast-pathing Black
types, (2) always recording in visit_node, (3) using visit_node from
visit_decl, and (4) visiting type arguments with under_ref=true.

Co-authored-by: Copilot <[email protected]>
The mangle_enum function creates composite names from (type_lid,
enum_lid) to disambiguate enum values across types. When the type at
the use site is a typedef alias rather than the canonical tag type,
mangle_enum produces a different name than at the definition site.

Fix by resolving type abbreviations before calling mangle_enum at
both the EEnum expression and SEnum switch case sites.

Co-authored-by: Copilot <[email protected]>
- DeclOrder.fst: Tests that non-polymorphic types used by value inside
  monomorphised polymorphic types are emitted in correct DFS order.
  Fails without commits d72e7fa and c105d05 (types emitted after
  their users, causing C compilation errors).

- EnumAliasResolve.fst + EnumAliasHelper.fst: Tests that enum values
  are correctly resolved when the type at the use site is a typedef
  alias. Two types share constructor names, causing the DataTypes pass
  to make one an abbreviation of the other. Fails without commit
  8acc4b3 (mangle_enum produces mismatched names for aliases).

Co-authored-by: Copilot <[email protected]>
@tahina-pro tahina-pro requested a review from protz February 18, 2026 21:13
@tahina-pro tahina-pro marked this pull request as ready for review February 18, 2026 21:14
@tahina-pro
Copy link
Member Author

Also shown to work well with Pulse: https://github.com/tahina-pro/FStar/actions/runs/22158831433/job/64073712693

@protz
Copy link
Collaborator

protz commented Feb 19, 2026

Thanks. The testcases are helpful but the code change seems like it doesn't address the root of the issue (stray abbreviations).

My suspicion is that this is a combination of optimizing data types representation (which generates type abbreviations that are not inlined away) and the enum mangling scheme taking the lid on the node at face value.

I'd rather insert another call to inline_type_abbrevs in the main driver to re-establish the invariant that there are no uses of type abbreviations and that subsequent passes do not need to worry about maintaining their own tables to keep track of equivalence classes.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants